Inference at * 
Iof proof for Lemma bnot-ff:


  a:. ((a) ~ ff)  (a ~ tt) 

latex

 by ((((D (0)) 
CollapseTHENA (Auto))) 
CCollapseTHEN (AutoBoolCase a)) 

latex

CC.

Definitions	left + right, Unit, , tt, p q, p  q, p  q, a < b, x f y, f(a), a < b, null(as), x =a y, (i = j), i z j, i <z j, p =b q, P  Q, P & Q, x:A  B(x), b, , Type, ff, x:A. B(x), b, P  Q, x:AB(x), A, , s = t, t  T, s ~ t
Lemmas	eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, assert wf, bool wf